package org.xteam.sled.semantic;

import java.util.ArrayList;
import java.util.HashSet;
import java.util.List;
import java.util.Set;

import org.xteam.sled.semantic.exp.Exp;
import org.xteam.sled.semantic.exp.ExpAdd;
import org.xteam.sled.semantic.exp.ExpCondition;
import org.xteam.sled.semantic.exp.ExpConst;
import org.xteam.sled.semantic.exp.ExpPC;
import org.xteam.sled.semantic.exp.ExpRewriter;
import org.xteam.sled.semantic.exp.IExpRewriter;
import org.xteam.sled.semantic.exp.VariableSubstitute;


public class Disjunct {
	
	private String name;
	private Set<Exp> conditions;
	private Sequence sequence;
	
	public Disjunct(Sequence sequence) {
		this(new HashSet<Exp>(), sequence);
	}
	
	public Disjunct(Set<Exp> conds, Sequence sequence) {
		this.sequence = sequence;
		this.conditions = conds;
	}
	
	public Disjunct(String name, Set<Exp> conds, Sequence sequence) {
		this.name = name;
		this.sequence = sequence;
		this.conditions = conds;
	}

	public String name() {
		return name;
	}
	
	public void setName(String name) {
		this.name = name;
	}
	
	public boolean hasConditions() {
		return conditions.size() > 0;
	}
	
	public void addConditions(List<ExpCondition> constraints) {
		conditions.addAll(constraints);
	}
	
	public Sequence getSequence() {
		return sequence;
	}
	
	public Disjunct and(Disjunct other) {
		int l1 = getSequence().bitLength();
		int l2 = other.getSequence().bitLength();
		int longest = Math.max(l1, l2);
		int pos1 = 0, pos2 = 0;
		Sequence newSeq = null;
		if ((getSequence().hasPrefix() || other.getSequence().hasPrefix())) {
			if (getSequence().hasSuffix() || other.getSequence().hasSuffix())
				throw new RuntimeException("Illegal conjunction; dots on both left and right");
			pos1 = longest - l1;
			pos1 = longest - l2;
			newSeq = getSequence().mergeRight(other.getSequence());
		} else {
			newSeq = getSequence().mergeLeft(other.getSequence());
		}
		Set<Exp> newConds = new HashSet<Exp>();
		addToPC(pos1, conditions, newConds);
		addToPC(pos2, other.conditions, newConds);
		return new Disjunct(newConds, newSeq);
	}
	
	public Disjunct seq(Disjunct other) {
		if (getSequence().hasSuffix() && allLocBindings(other.getSequence().getElements()))
			throw new RuntimeException("illegal concatenation `... ; L:'");
		if (other.getSequence().hasPrefix() && allLocBindings(getSequence().getElements()))
			throw new RuntimeException("illegal concatenation `L: ...'");
		int k = getSequence().bitLength();
		Set<Exp> newConds = new HashSet<Exp>();
		newConds.addAll(conditions);
		addToPC(k, other.conditions, newConds);
		List<SequenceElement> newElements = new ArrayList<SequenceElement>(getSequence().getElements());
		for (SequenceElement element : other.getSequence().getElements()) {
			newElements.add(element.substitutePC(k, addBitsToPC(k)));
		}
		Sequence newSeq = new Sequence(getSequence().hasPrefix(), other.getSequence().hasSuffix(), newElements);
		return new Disjunct(newConds, newSeq);
	}
	
	private boolean allLocBindings(List<SequenceElement> elements) {
		for (SequenceElement element : elements) {
			if (! element.isLabel())
				return false;
		}
		return false;
	}

	public Disjunct preDots() {
		return new Disjunct(name, conditions, sequence.preDots());
	}

	public Disjunct postDots() {
		return new Disjunct(name, conditions, sequence.postDost());
	}
	
	private int bitsToPCunits(int bits) {
		int unit = GlobalState.pcUnitBits;
	  	int pcs = bits / unit;
	  	if (pcs * unit != bits) {
	  		throw new RuntimeException("Token of size " + bits
	  				+ " is not integral number of " + unit + "-bit units used to increment PC");
	  	}
	  	return pcs;
	}
	
	private Exp addBitsToPC(int bits) {
		if (bits == 0)
			return new ExpPC();
		return new ExpAdd(new ExpPC(), new ExpConst(bitsToPCunits(bits)));
	}
    
    private Exp pcplus(int bits, Exp e) {
		if (bits == 0)
			return e;
		return new PCSubstitute(addBitsToPC(bits)).rewrite(e);
	}
    
    public static class PCSubstitute extends ExpRewriter {
    	
    	private Exp exp;

		public PCSubstitute(Exp exp) {
    		this.exp = exp;
    	}

		public void visitPC(ExpPC expPC) {
			stack.push(exp);
    	}
    }
    
  	private void addToPC (int pos, Set<Exp> conds, Set<Exp> result) {
		for (Exp e : conds) {
			result.add(pcplus(pos, e));
		}
	}
  	
  	public void makeLabelsPCRelative() {
  		VariableSubstitute subs = new VariableSubstitute(getSequence().labelOffsets());
  		Set<Exp> newConditions = new HashSet<Exp>();
  		for (Exp condition : conditions) {
  			newConditions.add(subs.rewrite(condition));
		}
  		conditions = newConditions;
  		getSequence().makePCRelative(subs);
	}
	
	public String toString() {
		StringBuffer buffer = new StringBuffer();
		if (name != null) {
			buffer.append(name);
			buffer.append(":");
		}
		if (conditions.size() > 0) {
			boolean isFirst = true;
			for (Exp cond : conditions) {
				if (isFirst)
					isFirst = false;
				else
					buffer.append(", ");
				buffer.append(cond.toString());
			}
		}
		buffer.append(sequence.toString());
		return buffer.toString();
	}

	public Disjunct subst(IExpRewriter subs) {
		Set<Exp> n = new HashSet<Exp>();
		for (Exp e : conditions) {
			e = subs.rewrite(e);
			if (e.isConst() /* && e == true */) {
				n.add(e);
				throw new RuntimeException("not completed");
			}
		}
		return new Disjunct(n, sequence.subst(subs));
	}

	public Set<Exp> getConditions() {
		return conditions;
	}

	public Disjunct injectLatent() {
		return new Disjunct(new HashSet<Exp>(conditions), sequence.injectLatent());
	}
	
	// apply on Labelled
	public Disjunct actualizeLatent(boolean actualsOk) {
		return new Disjunct(new HashSet<Exp>(conditions), sequence.actualize(actualsOk));
	}
			  	
	public Disjunct nameUnnamed(String newName) {
		if (name != null)
			return this;
		return new Disjunct(newName, new HashSet<Exp>(conditions), sequence);
	}
	
}
